$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $L$:($T$ List), $x$, $y$, $a$, $b$:$T$. $x$=$f$$\ast$($y$) via $L$ $\Rightarrow$ $a$ before $b$ $\in$ $L$ $\Rightarrow$ $a$ is $f$$\ast$($b$)